Nuprl Lemma : qadd-add
11,40
postcript
pdf
x
,
y
:
. (
x
+
y
) ~ (
x
+
y
)
latex
Definitions
Top
,
tt
,
if
b
then
t
else
f
fi
,
t
T
,
r
+
s
,
x
:
A
.
B
(
x
)
Lemmas
isint-int
origin
x, y:
. (x + y) ~ (x+y) x, y:. (x + y) ~ (x+y) 
Tx:A. B(x)